Nuprl Lemma : iseg_map
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
L1
,
L2
:(
A
List). iseg(
A
;
L1
;
L2
)
iseg(
B
; map(
f
;
L1
); map(
f
;
L2
))
latex
Definitions
prop{i:l}
,
t
T
,
x
:
A
.
B
(
x
)
,
iseg(
T
;
l1
;
l2
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
top
Lemmas
append
wf
,
map
wf
,
map
append
sq
origin
A,B:Type, f:(A
B), L1,L2:(A List). iseg(A; L1; L2) 
iseg(B; map(f; L1); map(f; L2)) A,B:Type, f:(AB), L1,L2:(A List). iseg(A; L1; L2) iseg(B; map(f; L1); map(f; L2)) 
T
x:A. B(x) Qx:A. B(x)